M:MsgA, k:Knd, l:IdLnk, tg:Id. M.sframe(k sends <l,tg>)  Prop 

latex

Definitions	MsgA, M.sframe(k sends <l,tg>), z != f(x)  P(a;z), x,y. t(x;y), product-deq(A;B;a;b), IdLnkDeq, IdDeq, Prop, deq-member(eq;x;L), KindDeq, b, x  dom(f), a:A fp B(a), x. t(x), x:A. B(x), Id, IdLnk, t  T, Knd
Lemmas	Knd wf, IdLnk wf, Id wf, fpf-trivial-subtype-top, fpf-dom wf, assert wf, Kind-deq wf, deq-member wf, id-deq wf, idlnk-deq wf, product-deq wf, fpf-val wf, msga wf